(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(push)
(push)
(assert (and v3 v4 v1 v6 v4 v3 v8 v11))
(declare-const v13 Bool)
(assert (=> (and v7 v3 v5 v1 v9 v12 v8 v5 v1 v4 v10) v7))
(assert (= v6 v13))
(push)
(declare-const v14 Bool)
(declare-const v15 Bool)
(assert (= (and (= #b1010110 #b1010110 #b1010110) v14 v7 (or v0 v12 v4 v9 v1 (distinct #b1010110 #b1010110 #b1010110 #b1010110 #b1010110) (= #b1010110 #b1010110 #b1010110) v2 (and v7 v3 v5 v1 v9 v12 v8 v5 v1 v4 v10) (=> (and v7 v3 v5 v1 v9 v12 v8 v5 v1 v4 v10) v7) v4) v14 v5) (=> v5 v6) v2 v13 v13))
(assert (not (and (= #b1010110 #b1010110 #b1010110) v14 v7 (or v0 v12 v4 v9 v1 (distinct #b1010110 #b1010110 #b1010110 #b1010110 #b1010110) (= #b1010110 #b1010110 #b1010110) v2 (and v7 v3 v5 v1 v9 v12 v8 v5 v1 v4 v10) (=> (and v7 v3 v5 v1 v9 v12 v8 v5 v1 v4 v10) v7) v4) v14 v5)))
(pop)
(assert v10)
(declare-const v16 Bool)
(assert v11)
(declare-const v17 Bool)
(declare-const v18 Bool)
(assert v3)
(check-sat)
